es:ES, Cmd:Type, In:AbsInterface(Cmd), isupdate:(Cmd), Sys, Out:AbsInterface(Top).
(E(In) r E(Sys))
 (f:sys-antecedent(es;Sys), chain:(E(Sys)(Id List)).
 chain-consistent(f;chain)
  (e, e':E(Sys). ((loc(e) = loc(e')  Id))  (loc(e) << loc(e')  loc(e') << loc(e)))) 

latex

Up	abstract chain replication
Definitions	t  T, b, E, x << y, A, s = t, {x:A| B(x)} , E(X), let x,y = A in B(x;y), t.1, x:AB(x), x:A. B(x), a:A fp B(a), strong-subtype(A;B), P  Q, ES, Type, AbsInterface(A), sys-antecedent(es;Sys), chain-consistent(f;chain), , type List, x:A  B(x), left + right, x:A. B(x), <a, b>, Id, P  Q, a < b, P & Q, hd(l), L1  L2, adjacent(T;L;x;y), no_repeats(T;l), x before y  l, !Void(), False, Top, loc(e), {T}, Atom$n, , Dec(P), P  Q, A  B, b | a, a ~ b, a  b, a <p b, a < b, A c B, f(a), x f y, xL. P(x), (xL.P(x)), r  s, r < s, q-rel(r;x), Outcome, (x  l), l_disjoint(T;l1;l2), (e <loc e'), e loc e' , (e < e'), e c e', e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), IdLnk, Knd, a = b, P  Q
Lemmas	chain-order-total, event system wf, bool wf, top wf, es-interface wf, sys-antecedent wf, chain-consistent wf, not functionality wrt iff, iff wf, rev implies wf, assert-eq-id, assert wf, eq id wf, false wf, not wf, Id wf, chain-order wf, es-loc wf, member wf, es-E wf, es-E-interface wf, subtype rel wf